\begin{tabbing}
$\forall$${\it poss}$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex](Trans $a$,$b$:possible{-}event\{i:l\}(${\it poss}$). $R$($a$,$b$))
\\[0ex]$\Rightarrow$ (\=$\forall$$P$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $e$:possible{-}event\{i:l\}(${\it poss}$).\+
\\[0ex]es{-}knows\=\{i:l\}\+
\\[0ex](${\it poss}$; $R$; $P$; $e$)
\-\\[0ex]$\Rightarrow$ es{-}knows\=\{i:l\}\+
\\[0ex](${\it poss}$; $R$; ($\lambda$$e$.es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e$)); $e$))
\-\-
\end{tabbing}